InforLorV4, Main, Exploration, bibRecord, 009F29

Behavioral Conformance Verification in an Integrated Approach Using UML and B

Identifieur interne : 009F29 ( Main/Exploration ); précédent : 009F28; suivant : 009F30

Behavioral Conformance Verification in an Integrated Approach Using UML and B

Auteurs : Eric Meyer [France] ; Thomas Santen [Allemagne]

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:7504E7E0004376A6D8340B347832229F61F2012D

Descripteurs français

Pascal (Inist)
- Dessin schématique, Langage modélisation unifiée (UML), Orienté objet, Polymorphisme, Spécification formelle.

English descriptors

KwdEn :
- Diagrammatic sketche, Formal specification, Object oriented, Polymorphism.

Abstract

Abstract: We propose an integration of diagrammatic object oriented modeling techniques with a formal specification and verification technique. We translate UML class diagrams to B abstract machines in a way that does not only provide a formal interpretation of the class diagrams but that also allows us to verify properties of object oriented models within the framework of the B method. Specifically, we address translating generalization / specialization hierarchies to B. An appropriate construction of B components allows us to express and formally verify behavioral conformance, which ensures that polymorphism can be used safely. Expressing the proof obligations associated with behavioral conformance by constructing B components makes it possible to use the tool AtelierB for mechanically verifying them.

Url:

https://api.istex.fr/ark:/67375/HCB-PS31JBQG-T/fulltext.pdf

DOI: 10.1007/3-540-40911-4_21

Affiliations:

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Behavioral Conformance Verification in an Integrated Approach Using UML and B</title>
<author><name sortKey="Meyer, Eric" sort="Meyer, Eric" uniqKey="Meyer E" first="Eric" last="Meyer">Eric Meyer</name>
</author>
<author><name sortKey="Santen, Thomas" sort="Santen, Thomas" uniqKey="Santen T" first="Thomas" last="Santen">Thomas Santen</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:7504E7E0004376A6D8340B347832229F61F2012D</idno>
<date when="2000" year="2000">2000</date>
<idno type="doi">10.1007/3-540-40911-4_21</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-PS31JBQG-T/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001A92</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001A92</idno>
<idno type="wicri:Area/Istex/Curation">001A72</idno>
<idno type="wicri:Area/Istex/Checkpoint">002182</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002182</idno>
<idno type="wicri:doubleKey">0302-9743:2000:Meyer E:behavioral:conformance:verification</idno>
<idno type="wicri:Area/Main/Merge">00A510</idno>
<idno type="wicri:source">INIST</idno>
<idno type="RBID">Pascal:01-0048676</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000991</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000085</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000A23</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000A23</idno>
<idno type="wicri:doubleKey">0302-9743:2000:Meyer E:behavioral:conformance:verification</idno>
<idno type="wicri:Area/Main/Merge">00A629</idno>
<idno type="wicri:Area/Main/Curation">009F29</idno>
<idno type="wicri:Area/Main/Exploration">009F29</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Behavioral Conformance Verification in an Integrated Approach Using UML and B</title>
<author><name sortKey="Meyer, Eric" sort="Meyer, Eric" uniqKey="Meyer E" first="Eric" last="Meyer">Eric Meyer</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA, Université Nancy 2, UMR 7503 Campus scientifique, BP 239, 54506, Vandæuvre-les-Nancy Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandæuvre-les-Nancy</settlement>
</placeName>
<orgName type="university">Université Nancy 2</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Santen, Thomas" sort="Santen, Thomas" uniqKey="Santen T" first="Thomas" last="Santen">Thomas Santen</name>
<affiliation wicri:level="3"><country>Allemagne</country>
<placeName><settlement type="city">Berlin</settlement>
<region type="land" nuts="2">Berlin</region>
</placeName>
<wicri:orgArea>Institut für Kommunikations- und Softwaretechnik, Technische Universität Berlin, Franklinstrasse 28/29, D-10587</wicri:orgArea>
</affiliation>
<affiliation><wicri:noCountry code="no comma">E-mail: santen@acm.org</wicri:noCountry>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Diagrammatic sketche</term>
<term>Formal specification</term>
<term>Object oriented</term>
<term>Polymorphism</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Dessin schématique</term>
<term>Langage modélisation unifiée (UML)</term>
<term>Orienté objet</term>
<term>Polymorphisme</term>
<term>Spécification formelle</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: We propose an integration of diagrammatic object oriented modeling techniques with a formal specification and verification technique. We translate UML class diagrams to B abstract machines in a way that does not only provide a formal interpretation of the class diagrams but that also allows us to verify properties of object oriented models within the framework of the B method. Specifically, we address translating generalization / specialization hierarchies to B. An appropriate construction of B components allows us to express and formally verify behavioral conformance, which ensures that polymorphism can be used safely. Expressing the proof obligations associated with behavioral conformance by constructing B components makes it possible to use the tool AtelierB for mechanically verifying them.</div>
</front>
</TEI>
<affiliations><list><country><li>Allemagne</li>
<li>France</li>
</country>
<region><li>Berlin</li>
<li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Berlin</li>
<li>Vandæuvre-les-Nancy</li>
</settlement>
<orgName><li>Université Nancy 2</li>
</orgName>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Meyer, Eric" sort="Meyer, Eric" uniqKey="Meyer E" first="Eric" last="Meyer">Eric Meyer</name>
</region>
<name sortKey="Meyer, Eric" sort="Meyer, Eric" uniqKey="Meyer E" first="Eric" last="Meyer">Eric Meyer</name>
</country>
<country name="Allemagne"><region name="Berlin"><name sortKey="Santen, Thomas" sort="Santen, Thomas" uniqKey="Santen T" first="Thomas" last="Santen">Thomas Santen</name>
</region>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 009F29 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 009F29 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:7504E7E0004376A6D8340B347832229F61F2012D
   |texte=   Behavioral Conformance Verification in an Integrated Approach Using UML and B
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

Serveur d'exploration sur la recherche en informatique en Lorraine

Behavioral Conformance Verification in an Integrated Approach Using UML and B

Behavioral Conformance Verification in an Integrated Approach Using UML and B

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.